Nuprl Lemma : es-Choose_wf
11,40
postcript
pdf
es
:ES. es-Choose(
es
)
i
,
a
:Id
state@
i
(?(es-V(
es
)(
i
,
a
)))
latex
Definitions
t
T
,
es-T(
es
)
,
vartype(
i
;
x
)
,
es-Choose(
es
)
,
es-V(
es
)
,
state@
i
,
x
:
A
B
(
x
)
,
ES
,
x
:
A
B
(
x
)
,
Id
,
,
Unit
,
f
(
a
)
,
left
+
right
,
x
:
A
.
B
(
x
)
Lemmas
event
system
wf
origin
es:ES. es-Choose(es) 
i,a:Id
state@i(?(es-V(es)(i,a))) es:ES. es-Choose(es) i,a:Idstate@i(?(es-V(es)(i,a))) T
B(x)B(x)x:A. B(x)